Test Sets for the Universal and Existential Closure of Regular Tree Languages
Identifieur interne : 00A929 ( Main/Exploration ); précédent : 00A928; suivant : 00A930Test Sets for the Universal and Existential Closure of Regular Tree Languages
Auteurs : Dieter Hofbauer [Allemagne] ; Maria Huber [Allemagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.
Url:
DOI: 10.1007/3-540-48685-2_16
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000442
- to stream Istex, to step Curation: 000439
- to stream Istex, to step Checkpoint: 002315
- to stream Main, to step Merge: 00AF81
- to stream Main, to step Curation: 00A929
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Test Sets for the Universal and Existential Closure of Regular Tree Languages</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></author><author><name sortKey="Huber, Maria" sort="Huber, Maria" uniqKey="Huber M" first="Maria" last="Huber">Maria Huber</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:13F30667E455B185376F3A71BCFCE8B7D5C718D7</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1007/3-540-48685-2_16</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-MN6G2JP7-P/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000442</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000442</idno><idno type="wicri:Area/Istex/Curation">000439</idno><idno type="wicri:Area/Istex/Checkpoint">002315</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002315</idno><idno type="wicri:doubleKey">0302-9743:1999:Hofbauer D:test:sets:for</idno><idno type="wicri:Area/Main/Merge">00AF81</idno><idno type="wicri:Area/Main/Curation">00A929</idno><idno type="wicri:Area/Main/Exploration">00A929</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Test Sets for the Universal and Existential Closure of Regular Tree Languages</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Universität GH Kassel, Fachbereich 17 Mathematik/Informatik, D-34109, Kassel</wicri:regionArea><placeName><region type="land" nuts="1">Hesse (Land)</region><region type="district" nuts="2">District de Kassel</region><settlement type="city">Cassel (Hesse)</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author><author><name sortKey="Huber, Maria" sort="Huber, Maria" uniqKey="Huber M" first="Maria" last="Huber">Maria Huber</name><affiliation wicri:level="3"><country xml:lang="fr">Allemagne</country><wicri:regionArea>Universität GH Kassel, Fachbereich 17 Mathematik/Informatik, D-34109, Kassel</wicri:regionArea><placeName><region type="land" nuts="1">Hesse (Land)</region><region type="district" nuts="2">District de Kassel</region><settlement type="city">Cassel (Hesse)</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Allemagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Finite test sets are a useful tool for deciding the membership problem for the universal closure of a given tree language, that is, for deciding whether a term has all its ground instances in the given language. A uniform test set for the universal closure must serve the following purpose: In order to decide membership of a term, it is sufficient to check whether all its test set instances belong to the underlying language. A possible application, and our main motivation, is ground reducibility, an essential concept for many approaches to inductive reasoning. Ground reducibility modulo some rewrite system is membership in the universal closure of the set of reducible ground terms. Here, test sets always exist, and several algorithmic approaches are known. The resulting sets, however, are often unnecessarily large. In this paper we consider regular languages and linear closure operators. We prove that universal as well as existential closure, defined analogously, preserve regularity. By relating test sets to tree automata and to appropriate congruence relations, we show how to characterize, how to compute, and how to minimize ground and non-ground test sets. In particular, optimal solutions now replace previous ad hoc approximations for the ground reducibility problem.</div></front></TEI><affiliations><list><country><li>Allemagne</li></country><region><li>District de Kassel</li><li>Hesse (Land)</li></region><settlement><li>Cassel (Hesse)</li></settlement></list><tree><country name="Allemagne"><region name="Hesse (Land)"><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></region><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><name sortKey="Huber, Maria" sort="Huber, Maria" uniqKey="Huber M" first="Maria" last="Huber">Maria Huber</name><name sortKey="Huber, Maria" sort="Huber, Maria" uniqKey="Huber M" first="Maria" last="Huber">Maria Huber</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A929 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 00A929 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:13F30667E455B185376F3A71BCFCE8B7D5C718D7
|texte= Test Sets for the Universal and Existential Closure of Regular Tree Languages
}}
| This area was generated with Dilib version V0.6.33. |  |